perm filename BOYERM.RE1[LET,JMC]1 blob
sn#544090 filedate 1980-10-22 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .require "let.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "let.pub[let,jmc]" source;
∂CSL Prof. A.G. Dale, Chairman↓Department of Computer Science
↓University of Texas↓Austin, Texas 78712∞
Dear Professor Dale:
I can recommend without qualification the appointment of
Dr. Robert S. Boyer and Dr. J Strother Moore II as associate
professors of computer science. In my opinion, they would have
had such positions some time ago if they weren't a package.
Here are my answers to the four questions in your letter of
October 17.
1. I think their book
%2A Computational Logic%1
is outstanding, because it is the first on theorem proving to
squarely face the problem of mathematical induction and also
because they have been able to apply their methods to more difficult
problems than have been done previously.
The work on mathematical induction may point the way to using
schemata in general, and my own work in non-monotonic reasoning
has convinced me that using schemata will be required for
all kinds of intelligent reasoning.
2. I am not currently an expert in the techniques of
theorem proving, because most of its practitioners are still
mainly involved with domain independent heuristics, and it is
very difficult to evaluate their success. It seems to me that
Boyer and Moore occupy a valuable intermediate position between
domain independent theorem proving and the ad hoc methods of
the people who work on expert systems.
I don't know whether their results can be ascribed to one or
the other of them, but I doubt it.
3. Their lectures at meetings are excellent, and I have
heard both of them lecture. I have no
other information about their teaching ability.
4. Adding the Boyer and Moore team to Bledsoe and Good should give
the University of Texas the best theorem proving group in the
world.
.sgn